ds:x:Id fp Type, da:k:Knd fp Type, v:ecl-trans-tuple{i:l}(ds;da).
ecl-trans-normal(v)  Prop 

latex

Definitions	t  T, , x:A. B(x), no_repeats(T;l), P  Q, sorted(L), P & Q, Prop, finite-type(T), b, A, , Dec(P), let a,b,c,d,e,f,g = u in v(a;b;c;d;e;f;g), ecl-trans-normal(x), ecl-trans-tuple{i:l}(ds;da), Id, x. t(x), a:A fp B(a), Knd
Lemmas	ecl-trans-tuple wf, Knd wf, fpf wf, Id wf, decidable wf, nat wf, not wf, assert wf, finite-type wf, sorted wf, no repeats wf, nat plus wf